$\forall$$a$:Atom. AtomFree(Atom;$a$)